perm filename MULT[EKL,SYS]3 blob sn#825733 filedate 1986-10-11 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the notion of multiplicity
C00006 00003	multiplicity of union is sum of multiplicities
C00010 ENDMK
C⊗;
;the notion of multiplicity

(wipe-out)
(get-proofs sums prf ekl sys)

(proof multiplicity)

(decl mult (type: |(ground⊗@set)→ground|) (syntype: constant))
(defax mult |∀x u a.mult(nil,a)=0∧
                    mult(x.u,a)=if a(x) then mult(u,a)' else mult(u,a)|)
(label mult_def)

;facts about multiplicity

(axiom |∀u a.natnum(mult(u,a))|)
(label simpinfo)(label multfact)

(axiom |∀u a.mult(u,a)≤length(u)|)
(label length_mult)

(axiom |∀u y a.member(y,u)∧a(y)⊃1≤mult(u,a)|) 
(label member_mult)

;Exercise:(not used in the proofs)
;(axiom |∀a u x.mult(u,a)≤mult(x.u,a)|)
;(label simpinfo)(label multfact)

(axiom |∀a u n.n<length(u)⊃mult(nthcdr(u,n),a)≤mult(u,a)|)
(label mult_nthcdr)

(axiom |∀u.mult(u,emptyset)=0|)
(label simpinfo)(label emptyfacts)

(axiom |∀v i j.i<j∧j<length v∧nth(v,i)=nth(v,j)⊃
               2≤mult(v,mkset(nth(v,i)))|)
(label multinj_computation)

(axiom |∀v.(∀k.k<length v⊃mult(v,mkset(nth(v,k)))=1)⊃inj(v)|)
(label mult_inj)
;multiplicity of union is sum of multiplicities
(proof mult_of_un_is_sum_un)

(axiom |∀u a b.disj_pair(a,b)⊃mult(u,a∪b)=mult(u,a)+mult(u,b)|)
(label multsum)

(axiom |∀setseq u n.disjoint(setseq,n)⊃
                    mult(u,un(setseq,n))=sum(λm.mult(u,setseq(m)),n)|)
(label mult_of_un_is_sum_mult)
(save-proofs mult)